Left Termination of the query pattern
mult(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 85 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 129 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES

(0) Obligation:

Clauses:

mult(X1, 0, 0).
mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z)).
sum(X, 0, X).
sum(X, s(Y), s(Z)) :- sum(X, Y, Z).

Query: mult(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

sumA(s(X1), s(X2)) :- sumA(X1, X2).
multB(X1, s(X2), X3) :- multB(X1, X2, X4).
multB(X1, s(X2), X3) :- ','(multcB(X1, X2, X4), sumC(X4, X1, X3)).
sumC(X1, s(X2), s(X3)) :- sumC(X1, X2, X3).
sumD(X1, s(X2), s(X3)) :- sumD(X1, X2, X3).
multE(X1, s(0), X2) :- sumA(X1, X2).
multE(X1, s(s(X2)), X3) :- multB(X1, X2, X4).
multE(X1, s(s(X2)), X3) :- ','(multcB(X1, X2, X4), sumC(X4, X1, X5)).
multE(X1, s(s(X2)), X3) :- ','(multcB(X1, X2, X4), ','(sumcC(X4, X1, X5), sumD(X5, X1, X3))).

Clauses:

sumcA(0, 0).
sumcA(s(X1), s(X2)) :- sumcA(X1, X2).
multcB(X1, 0, 0).
multcB(X1, s(X2), X3) :- ','(multcB(X1, X2, X4), sumcC(X4, X1, X3)).
sumcC(X1, 0, X1).
sumcC(X1, s(X2), s(X3)) :- sumcC(X1, X2, X3).
sumcD(X1, 0, X1).
sumcD(X1, s(X2), s(X3)) :- sumcD(X1, X2, X3).

Afs:

multE(x1, x2, x3)  =  multE(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
multE_in: (b,b,f)
sumA_in: (b,f)
multB_in: (b,b,f)
multcB_in: (b,b,f)
sumcC_in: (b,b,f)
sumC_in: (b,b,f)
sumD_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GGA(X1, s(0), X2) → U7_GGA(X1, X2, sumA_in_ga(X1, X2))
MULTE_IN_GGA(X1, s(0), X2) → SUMA_IN_GA(X1, X2)
SUMA_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, sumA_in_ga(X1, X2))
SUMA_IN_GA(s(X1), s(X2)) → SUMA_IN_GA(X1, X2)
MULTE_IN_GGA(X1, s(s(X2)), X3) → U8_GGA(X1, X2, X3, multB_in_gga(X1, X2, X4))
MULTE_IN_GGA(X1, s(s(X2)), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U2_GGA(X1, X2, X3, multB_in_gga(X1, X2, X4))
MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U3_GGA(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U4_GGA(X1, X2, X3, sumC_in_gga(X4, X1, X3))
U3_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → SUMC_IN_GGA(X4, X1, X3)
SUMC_IN_GGA(X1, s(X2), s(X3)) → U5_GGA(X1, X2, X3, sumC_in_gga(X1, X2, X3))
SUMC_IN_GGA(X1, s(X2), s(X3)) → SUMC_IN_GGA(X1, X2, X3)
MULTE_IN_GGA(X1, s(s(X2)), X3) → U9_GGA(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U9_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U10_GGA(X1, X2, X3, sumC_in_gga(X4, X1, X5))
U9_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → SUMC_IN_GGA(X4, X1, X5)
U9_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_GGA(X1, X2, X3, sumcC_in_gga(X4, X1, X5))
U11_GGA(X1, X2, X3, sumcC_out_gga(X4, X1, X5)) → U12_GGA(X1, X2, X3, sumD_in_gga(X5, X1, X3))
U11_GGA(X1, X2, X3, sumcC_out_gga(X4, X1, X5)) → SUMD_IN_GGA(X5, X1, X3)
SUMD_IN_GGA(X1, s(X2), s(X3)) → U6_GGA(X1, X2, X3, sumD_in_gga(X1, X2, X3))
SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U15_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U15_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U16_gga(X1, X2, X3, sumcC_in_gga(X4, X1, X3))
sumcC_in_gga(X1, 0, X1) → sumcC_out_gga(X1, 0, X1)
sumcC_in_gga(X1, s(X2), s(X3)) → U17_gga(X1, X2, X3, sumcC_in_gga(X1, X2, X3))
U17_gga(X1, X2, X3, sumcC_out_gga(X1, X2, X3)) → sumcC_out_gga(X1, s(X2), s(X3))
U16_gga(X1, X2, X3, sumcC_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multcB_in_gga(x1, x2, x3)  =  multcB_in_gga(x1, x2)
multcB_out_gga(x1, x2, x3)  =  multcB_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumcC_in_gga(x1, x2, x3)  =  sumcC_in_gga(x1, x2)
sumcC_out_gga(x1, x2, x3)  =  sumcC_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
sumC_in_gga(x1, x2, x3)  =  sumC_in_gga(x1, x2)
sumD_in_gga(x1, x2, x3)  =  sumD_in_gga(x1, x2)
MULTE_IN_GGA(x1, x2, x3)  =  MULTE_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUMC_IN_GGA(x1, x2, x3)  =  SUMC_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUMD_IN_GGA(x1, x2, x3)  =  SUMD_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GGA(X1, s(0), X2) → U7_GGA(X1, X2, sumA_in_ga(X1, X2))
MULTE_IN_GGA(X1, s(0), X2) → SUMA_IN_GA(X1, X2)
SUMA_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, sumA_in_ga(X1, X2))
SUMA_IN_GA(s(X1), s(X2)) → SUMA_IN_GA(X1, X2)
MULTE_IN_GGA(X1, s(s(X2)), X3) → U8_GGA(X1, X2, X3, multB_in_gga(X1, X2, X4))
MULTE_IN_GGA(X1, s(s(X2)), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U2_GGA(X1, X2, X3, multB_in_gga(X1, X2, X4))
MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U3_GGA(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U3_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U4_GGA(X1, X2, X3, sumC_in_gga(X4, X1, X3))
U3_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → SUMC_IN_GGA(X4, X1, X3)
SUMC_IN_GGA(X1, s(X2), s(X3)) → U5_GGA(X1, X2, X3, sumC_in_gga(X1, X2, X3))
SUMC_IN_GGA(X1, s(X2), s(X3)) → SUMC_IN_GGA(X1, X2, X3)
MULTE_IN_GGA(X1, s(s(X2)), X3) → U9_GGA(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U9_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U10_GGA(X1, X2, X3, sumC_in_gga(X4, X1, X5))
U9_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → SUMC_IN_GGA(X4, X1, X5)
U9_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_GGA(X1, X2, X3, sumcC_in_gga(X4, X1, X5))
U11_GGA(X1, X2, X3, sumcC_out_gga(X4, X1, X5)) → U12_GGA(X1, X2, X3, sumD_in_gga(X5, X1, X3))
U11_GGA(X1, X2, X3, sumcC_out_gga(X4, X1, X5)) → SUMD_IN_GGA(X5, X1, X3)
SUMD_IN_GGA(X1, s(X2), s(X3)) → U6_GGA(X1, X2, X3, sumD_in_gga(X1, X2, X3))
SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U15_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U15_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U16_gga(X1, X2, X3, sumcC_in_gga(X4, X1, X3))
sumcC_in_gga(X1, 0, X1) → sumcC_out_gga(X1, 0, X1)
sumcC_in_gga(X1, s(X2), s(X3)) → U17_gga(X1, X2, X3, sumcC_in_gga(X1, X2, X3))
U17_gga(X1, X2, X3, sumcC_out_gga(X1, X2, X3)) → sumcC_out_gga(X1, s(X2), s(X3))
U16_gga(X1, X2, X3, sumcC_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multcB_in_gga(x1, x2, x3)  =  multcB_in_gga(x1, x2)
multcB_out_gga(x1, x2, x3)  =  multcB_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumcC_in_gga(x1, x2, x3)  =  sumcC_in_gga(x1, x2)
sumcC_out_gga(x1, x2, x3)  =  sumcC_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
sumC_in_gga(x1, x2, x3)  =  sumC_in_gga(x1, x2)
sumD_in_gga(x1, x2, x3)  =  sumD_in_gga(x1, x2)
MULTE_IN_GGA(x1, x2, x3)  =  MULTE_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUMC_IN_GGA(x1, x2, x3)  =  SUMC_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUMD_IN_GGA(x1, x2, x3)  =  SUMD_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U15_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U15_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U16_gga(X1, X2, X3, sumcC_in_gga(X4, X1, X3))
sumcC_in_gga(X1, 0, X1) → sumcC_out_gga(X1, 0, X1)
sumcC_in_gga(X1, s(X2), s(X3)) → U17_gga(X1, X2, X3, sumcC_in_gga(X1, X2, X3))
U17_gga(X1, X2, X3, sumcC_out_gga(X1, X2, X3)) → sumcC_out_gga(X1, s(X2), s(X3))
U16_gga(X1, X2, X3, sumcC_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multcB_in_gga(x1, x2, x3)  =  multcB_in_gga(x1, x2)
multcB_out_gga(x1, x2, x3)  =  multcB_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumcC_in_gga(x1, x2, x3)  =  sumcC_in_gga(x1, x2)
sumcC_out_gga(x1, x2, x3)  =  sumcC_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUMD_IN_GGA(x1, x2, x3)  =  SUMD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMD_IN_GGA(x1, x2, x3)  =  SUMD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUMD_IN_GGA(X1, s(X2)) → SUMD_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUMD_IN_GGA(X1, s(X2)) → SUMD_IN_GGA(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMC_IN_GGA(X1, s(X2), s(X3)) → SUMC_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U15_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U15_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U16_gga(X1, X2, X3, sumcC_in_gga(X4, X1, X3))
sumcC_in_gga(X1, 0, X1) → sumcC_out_gga(X1, 0, X1)
sumcC_in_gga(X1, s(X2), s(X3)) → U17_gga(X1, X2, X3, sumcC_in_gga(X1, X2, X3))
U17_gga(X1, X2, X3, sumcC_out_gga(X1, X2, X3)) → sumcC_out_gga(X1, s(X2), s(X3))
U16_gga(X1, X2, X3, sumcC_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multcB_in_gga(x1, x2, x3)  =  multcB_in_gga(x1, x2)
multcB_out_gga(x1, x2, x3)  =  multcB_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumcC_in_gga(x1, x2, x3)  =  sumcC_in_gga(x1, x2)
sumcC_out_gga(x1, x2, x3)  =  sumcC_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUMC_IN_GGA(x1, x2, x3)  =  SUMC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMC_IN_GGA(X1, s(X2), s(X3)) → SUMC_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMC_IN_GGA(x1, x2, x3)  =  SUMC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUMC_IN_GGA(X1, s(X2)) → SUMC_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUMC_IN_GGA(X1, s(X2)) → SUMC_IN_GGA(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)

The TRS R consists of the following rules:

multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U15_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U15_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U16_gga(X1, X2, X3, sumcC_in_gga(X4, X1, X3))
sumcC_in_gga(X1, 0, X1) → sumcC_out_gga(X1, 0, X1)
sumcC_in_gga(X1, s(X2), s(X3)) → U17_gga(X1, X2, X3, sumcC_in_gga(X1, X2, X3))
U17_gga(X1, X2, X3, sumcC_out_gga(X1, X2, X3)) → sumcC_out_gga(X1, s(X2), s(X3))
U16_gga(X1, X2, X3, sumcC_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multcB_in_gga(x1, x2, x3)  =  multcB_in_gga(x1, x2)
multcB_out_gga(x1, x2, x3)  =  multcB_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumcC_in_gga(x1, x2, x3)  =  sumcC_in_gga(x1, x2)
sumcC_out_gga(x1, x2, x3)  =  sumcC_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(X1, s(X2)) → MULTB_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTB_IN_GGA(X1, s(X2)) → MULTB_IN_GGA(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMA_IN_GA(s(X1), s(X2)) → SUMA_IN_GA(X1, X2)

The TRS R consists of the following rules:

multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U15_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U15_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U16_gga(X1, X2, X3, sumcC_in_gga(X4, X1, X3))
sumcC_in_gga(X1, 0, X1) → sumcC_out_gga(X1, 0, X1)
sumcC_in_gga(X1, s(X2), s(X3)) → U17_gga(X1, X2, X3, sumcC_in_gga(X1, X2, X3))
U17_gga(X1, X2, X3, sumcC_out_gga(X1, X2, X3)) → sumcC_out_gga(X1, s(X2), s(X3))
U16_gga(X1, X2, X3, sumcC_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multcB_in_gga(x1, x2, x3)  =  multcB_in_gga(x1, x2)
multcB_out_gga(x1, x2, x3)  =  multcB_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumcC_in_gga(x1, x2, x3)  =  sumcC_in_gga(x1, x2)
sumcC_out_gga(x1, x2, x3)  =  sumcC_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMA_IN_GA(s(X1), s(X2)) → SUMA_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUMA_IN_GA(s(X1)) → SUMA_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUMA_IN_GA(s(X1)) → SUMA_IN_GA(X1)
    The graph contains the following edges 1 > 1

(34) YES